Nuprl Lemma : R-size-decreases 0,22
A:Realizer. Rplus?(A)  {R-size(Rplus-left(A))<R-size(A) & R-size(Rplus-right(A))<R-size(A)} 
latex

Definitionsx:A. B(x), P  Q, b, Rplus?(x1), {T}, P & Q, R-size(R), Rplus-left(x1), Rplus-right(x1), Prop, x. t(x), t  T, false, if b t else f fi, x(s), , False
Lemmases realizer-induction, assert wf, Rplus? wf, guard wf, R-size wf, Rplus-left wf, nat plus wf, Rplus-right wf, es realizer wf, false wf, Rplus wf, Id wf, Knd wf, IdLnk wf, decl-state wf, decl-type wf, fpf wf

origin